I'm lost, didn't we said that bullet lists would be easier to use?
Otherwise, for what it's worth, as far as I remember, if we want to save characters, the last | at the end of the line is not mandatory (as well as the space before the first one).

I'm lost, didn't we said that bullet lists would be easier to use?

Yes, but also that we should try to use tables when reasonable.

Did we converge on some "definition" of reasonable?

Did we converge on some "definition" of reasonable?

I think that "unreasonable" was implicitly defined as "when formatting is too painful because there are many RHS that require several lines each"

Mmmhhh, I am concerned by the fact that the source file is much less readable.
In https://github.com/math-comp/analysis/blob/master/classical/classical_sets.v, we only used a table to format a summary of the documentation, and then providing the full documentation in verbatim centered lists (this was really just a test).
What about doing the same here? (LaTeXified digest at the top, and full doc in ASCII.)

The last commit has restored the detailed documentation and kept the table as well, which acts a a digest of the detailed documentation: this provides an overview of the documentation while keeping the source code file readable.

arg, the last commit was rejected, looks I do not have the rights to push @yoshihiro503

@yoshihiro503 I PRed to your PR instead